Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		f(x,0,0)	→ s(x)
2:		f(0,y,0)	→ s(y)
3:		f(0,0,z)	→ s(z)
4:		f(s(0),y,z)	→ f(0,s(y),s(z))
5:		f(s(x),s(y),0)	→ f(x,y,s(0))
6:		f(s(x),0,s(z))	→ f(x,s(0),z)
7:		f(0,s(0),s(0))	→ s(s(0))
8:		f(s(x),s(y),s(z))	→ f(x,y,f(s(x),s(y),z))
9:		f(0,s(s(y)),s(0))	→ f(0,y,s(0))
10:		f(0,s(0),s(s(z)))	→ f(0,s(0),z)
11:		f(0,s(s(y)),s(s(z)))	→ f(0,y,f(0,s(s(y)),s(z)))

There are 9 dependency pairs:


12:		F(s(0),y,z)	→ F(0,s(y),s(z))
13:		F(s(x),s(y),0)	→ F(x,y,s(0))
14:		F(s(x),0,s(z))	→ F(x,s(0),z)
15:		F(s(x),s(y),s(z))	→ F(x,y,f(s(x),s(y),z))
16:		F(s(x),s(y),s(z))	→ F(s(x),s(y),z)
17:		F(0,s(s(y)),s(0))	→ F(0,y,s(0))
18:		F(0,s(0),s(s(z)))	→ F(0,s(0),z)
19:		F(0,s(s(y)),s(s(z)))	→ F(0,y,f(0,s(s(y)),s(z)))
20:		F(0,s(s(y)),s(s(z)))	→ F(0,s(s(y)),s(z))

The approximated dependency graph contains 4 SCCs: {18}, {17}, {19,20} and {13-16}.

Consider the SCC {18}. There are no usable rules. By taking the AF π with π(F) = 3 together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(F) = 2 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {19,20}. By taking the AF π with π(F) = 2 together with the lexicographic path order with precedence f ≻ s, rule 20 is weakly decreasing and the rules in {1-11,19} are strictly decreasing. There is one new SCC.
- Consider the SCC {20}. There are no usable rules. By taking the AF π with π(F) = 3 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {13-16}. By taking the AF π with π(F) = 1 together with the lexicographic path order with precedence f ≻ s, rule 16 is weakly decreasing and the rules in {1-11,13-15} are strictly decreasing. There is one new SCC.
- Consider the SCC {16}. There are no usable rules. By taking the AF π with π(F) = 3 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.13 seconds) --- May 4, 2006